The Web SSO Standard OpenID Connect: In-Depth Formal Security Analysis and Security Guidelines

摘要

Web-based single sign-on (SSO) services such as Google Sign-In and Log Inwith Paypal are based on the OpenID Connect protocol. This protocol enablesso-called relying parties to delegate user authentication to so-called identityproviders. OpenID Connect is one of the newest and most widely deployed singlesign-on protocols on the web. Despite its importance, it has not received muchattention from security researchers so far, and in particular, has notundergone any rigorous security analysis. In this paper, we carry out the first in-depth security analysis of OpenIDConnect. To this end, we use a comprehensive generic model of the web todevelop a detailed formal model of OpenID Connect. Based on this model, we thenprecisely formalize and prove central security properties for OpenID Connect,including authentication, authorization, and session integrity properties. In our modeling of OpenID Connect, we employ security measures in order toavoid attacks on OpenID Connect that have been discovered previously and newattack variants that we document for the first time in this paper. Based onthese security measures, we propose security guidelines for implementors ofOpenID Connect. Our formal analysis demonstrates that these guidelines are infact effective and sufficient.